/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.bool;
import java.io.BufferedWriter;
import java.io.File;
import java.io.FileWriter;
import java.io.IOException;
import java.io.OutputStream;
import java.io.OutputStreamWriter;
import java.io.PrintWriter;
import java.util.HashMap;
import java.util.Iterator;
import java.util.List;
import java.util.ListIterator;
import java.util.Map;

import alloy.util.Dbg;

/**
 * Visitor to write out the formula in an extension of the DIMACS .sat input format.
 * NOTE: Documentation for this class is incomplete!
 * Input format is:
 * <p>
 * p sat nvars
 * expr
 * <p>
 * where
 * <p>
 * expr := lit | and | or | not | ref
 * num := [1-9][0-9]*
 * lit := num | -num
 * and := *( exprlist )
 * or := +( expr )
 * not := -( expr )
 * ref := [ num ]
 * <p>
 * where each open parenethesis ('(') increments the node id counter, with the first
 * opening parenthesis having id of 0, and backreferences (ref) refer to the node
 * corresponding to the counter.  of course, [ 0 ] cannot appear because no node
 * can backreference the outermost node.
 * <p>
 * Constants are written out as +(1 -1) for true and *(1 -1) for false.
 * <p>
 * The forXXXX methods return null.
 *
 * Example of usage:
 *
 *      WriteSAT_V wsv = new WriteSAT_V(fname, getNumVars());
 *      gbf.acceptVisitor(wsv);
 *      wsv.close();
 * <p>
 * C++ code to read files in this format is in the class BL_Manu.
 */
class WriteSAT_V extends GBF_V {
    private PrintWriter w;
  private Map _alloyVarIds = new HashMap();

    private  boolean _insideArg;

  private int _getAlloyVarId(BoolSwitch alloyVar_) {
    Integer id = (Integer)_alloyVarIds.get(alloyVar_);
    if (id == null) {
      _alloyVarIds.put(alloyVar_, id = new Integer(_alloyVarIds.size()));
      //System.out.println(alloyVar_ + " -> " + id);
    }
    return id.intValue();
  }

    /** The node ID of the node currently being visited.  Any future backreferences to this node
    will use this ID, which will be stored on the node (in {@link BooleanFormula#satFileNodeId}). */
    private int satFileNodeId = 0;
    private int indentLevel = 0;

    private void indent() {
    //for (int i=0; i<indentLevel; i++)
        w.print(" ");
    }

    /** Check whether the node represents an expression we have already written.
    This is the case if we have already visited this node with this visitor,
    <em>and</em>
    if yes, write to {@link #w} the backreference & return true;
    else, return false */
    private boolean checkSeen(BooleanFormula node_) {
    if (alreadyVisited(node_)) {
        w.print("[" + node_.satFileNodeId + "]");
        return true;
    }
    else {
        node_.satFileNodeId = this.satFileNodeId++;
        return false;
    }
    }

    WriteSAT_V(File fHandle, int nvars, boolean[] dependentVars_) {
    try {
      w = new PrintWriter(new BufferedWriter(new FileWriter(fHandle), 1024*1024));
    }
    catch (IOException e) {
      Dbg.chk(false, "Could not open " + fHandle + ": " + e);
      throw new Error("could not open "+fHandle+": "+e);
    }
    w.println("p sat " + new Integer(nvars));
    if (dependentVars_ != null)
        for (int i=1; i<dependentVars_.length; i++)
        if (dependentVars_[i])
            w.println("dep " + i);
    }

    WriteSAT_V(OutputStream out_) {
    w = new PrintWriter(new BufferedWriter(new OutputStreamWriter(out_), 1024*1024));
    }

    void close() { w.close(); w = null; }
    void flush() { w.println(); w.flush(); }

    Object forConst(GBF_Const g_const) { w.print(g_const.val ? "T" : "F"); return null; }

    Object forSetVarExpr(SetVarExpr setVarExpr_) {
    _chkDescr(setVarExpr_);
    if (!checkSeen(setVarExpr_)) {
        _checkCacheStart(setVarExpr_);
        w.print("!(" + setVarExpr_.getNodeSrc() + " " + _getAlloyVarId(setVarExpr_.var) + " " +
            setVarExpr_.val + " ");
        //  setVarExpr_.var.setVarValue(setVarExpr_.val);
        indentLevel += 2;
        setVarExpr_.expr.acceptVisitor(this);
        indentLevel -= 2;
        w.print(")");
        _checkCacheEnd(setVarExpr_);
    }
    return null;
    }

    Object forVarConst(VarConst varConst_)
    {
    _chkDescr(varConst_);
      w.print("#(" + _getAlloyVarId(varConst_.var) + " " + varConst_.val + ")");
      return null;
      //w.print(varConst_.var.getVarValue() == varConst_.val ? "T" : "F"); return null;
    }

    Object forLit(GBF_Lit g_lit) { _chkDescr(g_lit); w.print(g_lit.getLit()); return null; }

    Object forNot(GBF_Not g_not) {
    _chkDescr(g_not);
    if (!checkSeen(g_not)) {
        _checkCacheStart(g_not);
        w.print("-(");
        w.print(g_not.getNodeSrc());
        w.print(" ");
        indentLevel += 2;
        g_not.getExpr().acceptVisitor(this);
        indentLevel -= 2;
        w.print(")");
        _checkCacheEnd(g_not);
    }
    return null;
    }

    private void _chkDescr(BooleanFormula f_) {
//  if (f_.getDescr()!=null)
//      w.print(" %" + f_.getDescr() + "% ");
    }

    private Object _forAndOr(GBF_AndOrBase g_andor, String op) {
    BooleanFormula[] subexprs = g_andor.subexprs;
    if (subexprs.length == 0) {
        System.out.println("EMPTY ARRAY!");
        throw new Error("empty array!");
    }
    _chkDescr(g_andor);
    if (!checkSeen(g_andor)) {
        _checkCacheStart(g_andor);
        w.print(op+"(");
        w.print(g_andor.getNodeSrc());
        w.print(" ");
        indentLevel+=2;
        for (int i=0; i<subexprs.length; i++) {
        //w.println();
          indent();
          subexprs[i].acceptVisitor(this);
        }
        indentLevel-=2;
        w.print(")");
        _checkCacheEnd(g_andor);
    }
    return null;
    }
    Object forAnd(GBF_And g_and) { return _forAndOr(g_and, "*"); }
    Object forOr(GBF_Or g_or) { return _forAndOr(g_or, "+"); }

    Object forCNFFunc(CNFFunc cnfFunc_) {
    if (!checkSeen(cnfFunc_)) {
        _checkCacheStart(cnfFunc_);
        w.print("C(");
        List /* of int[] */ clauses = cnfFunc_.clauses;
        w.print(clauses.size());
        for (Iterator clauseIter = clauses.iterator(); clauseIter.hasNext();) {
        int[] clause = (int[])clauseIter.next();
        for (int j=0; j<clause.length; j++) {
            w.print(" "); w.print(clause[j]);
        }
        w.print(" 0");
        }
        w.print(" ");
        for (int i=0; i<cnfFunc_.subexprs.length; i++) {
        indent();
        cnfFunc_.subexprs[i].acceptVisitor(this);
        }
        w.print(")");
        _checkCacheEnd(cnfFunc_);
    }
    return null;
    }

  private void _checkCacheStart(BooleanFormula f_) { //if(true) return;
    //System.out.println("f@" + System.identityHashCode(f_) + "=" + f_);
    if (f_.getBoolTemplInsts().isEmpty()) return;
    //System.out.println("_checkCacheStart: " + f_);
    Dbg.chk(!_insideArg);
    for (Iterator instIter = f_.getBoolTemplInsts().iterator(); instIter.hasNext();) {
        BoolTemplateInstance inst = (BoolTemplateInstance)instIter.next();
        w.print("@(" + inst.templCacheId + " ");
        indentLevel += 2;
        //w.println();
        indent();
    }
    }

  private void _checkCacheEnd(BooleanFormula f_) { //if(true) return;
    if (f_.getBoolTemplInsts().isEmpty()) return;
    //System.out.println("_checkCacheEnd: " + f_);
    //w.println();
    for (ListIterator instIter =
         f_.getBoolTemplInsts().listIterator(f_.getBoolTemplInsts().size());
         instIter.hasPrevious();) {
        BoolTemplateInstance inst = (BoolTemplateInstance)instIter.previous();

        indent();
        w.print(inst.templArgScopes.length);
        indent();
        for (int i=0; i<inst.templArgScopes.length; i++) {
        w.print(inst.templArgScopes[i]); indent();
        }

        indent();
        for (int i=0; i<inst.templArgMults.length; i++) {
        w.print(inst.templArgMults[i]); indent();
        }
        indent();

        for (int i=0; i<inst.templCacheKey.length; i++) {
        Dbg.chk(inst.templCacheKey[i] != f_);
        Dbg.chk(!_insideArg);
	Dbg.chk(inst.templCacheKey[i].isConstantValued());
        _insideArg = true;
        inst.templCacheKey[i].acceptVisitor(this);
        Dbg.chk(_insideArg);
        _insideArg = false;
        //w.print();
        indent();

        }
        indentLevel -= 2;
        w.print(") ");
        indent();
    }
    }
}


